/-
Copyright (c) 2021 Alex Zhao. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Alex Zhao, Daniel Buth, Sebastian Meier, Junyan Xu
-/
import Mathlib.RingTheory.Ideal.NatInt

/-!
# Frobenius Number

In this file we first define a predicate for Frobenius numbers, then solve the 2-variable variant
of this problem. We also show the Frobenius number exists for any set of coprime natural numbers
that doesn't contain 1. This is closely related to the fact that all ideals of ℕ are finitely
generated, which we also prove in this file.

## Theorem Statement

Given a finite set of relatively prime integers all greater than 1, their Frobenius number is the
largest positive integer that cannot be expressed as a sum of nonnegative multiples of these
integers. Here we show the Frobenius number of two relatively prime integers `m` and `n` greater
than 1 is `m * n - m - n`. This result is also known as the Chicken McNugget Theorem.

## Implementation Notes

First we define Frobenius numbers in general using `IsGreatest` and `AddSubmonoid.closure`. Then
we proceed to compute the Frobenius number of `m` and `n`.

For the upper bound, we begin with an auxiliary lemma showing `m * n` is not attainable, then show
`m * n - m - n` is not attainable. Then for the construction, we create a `k_1` which is `k mod n`
and `0 mod m`, then show it is at most `k`. Then `k_1` is a multiple of `m`, so `(k-k_1)`
is a multiple of n, and we're done.

## Tags

frobenius number, chicken mcnugget, chinese remainder theorem, AddSubmonoid.closure
-/


open Nat

/-- A natural number `n` is the **Frobenius number** of a set of natural numbers `s` if it is an
upper bound on the complement of the additive submonoid generated by `s`.
In other words, it is the largest number that cannot be expressed as a sum of numbers in `s`. -/
def FrobeniusNumber (n : ℕ) (s : Set ℕ) : Prop :=
  IsGreatest { k | k ∉ AddSubmonoid.closure s } n

theorem frobeniusNumber_iff {n : ℕ} {s : Set ℕ} :
    FrobeniusNumber n s ↔ n ∉ AddSubmonoid.closure s ∧ ∀ k > n, k ∈ AddSubmonoid.closure s := by
  simp_rw [FrobeniusNumber, IsGreatest, upperBounds, Set.mem_setOf, not_imp_comm, not_le]

variable {m n : ℕ}

/-- The **Chicken McNugget theorem** stating that the Frobenius number
  of positive numbers `m` and `n` is `m * n - m - n`. -/
theorem frobeniusNumber_pair (cop : Coprime m n) (hm : 1 < m) (hn : 1 < n) :
    FrobeniusNumber (m * n - m - n) {m, n} := by
  simp_rw [FrobeniusNumber, AddSubmonoid.mem_closure_pair]
  have hmn : m + n ≤ m * n := add_le_mul hm hn
  constructor
  · push_neg
    intro a b h
    apply cop.mul_add_mul_ne_mul (add_one_ne_zero a) (add_one_ne_zero b)
    simp only [Nat.sub_sub, smul_eq_mul] at h
    zify [hmn] at h ⊢
    rw [← sub_eq_zero] at h ⊢
    rw [← h]
    ring
  · intro k hk
    dsimp at hk
    contrapose! hk
    let x := chineseRemainder cop 0 k
    have hx : x.val < m * n := chineseRemainder_lt_mul cop 0 k (ne_bot_of_gt hm) (ne_bot_of_gt hn)
    suffices key : x.1 ≤ k by
      obtain ⟨a, ha⟩ := modEq_zero_iff_dvd.mp x.2.1
      obtain ⟨b, hb⟩ := (modEq_iff_dvd' key).mp x.2.2
      exact ⟨a, b, by rw [mul_comm, ← ha, mul_comm, ← hb, Nat.add_sub_of_le key]⟩
    refine ModEq.le_of_lt_add x.2.2 (lt_of_le_of_lt ?_ (add_lt_add_right hk n))
    rw [Nat.sub_add_cancel (le_tsub_of_add_le_left hmn)]
    exact
      ModEq.le_of_lt_add
        (x.2.1.trans (modEq_zero_iff_dvd.mpr (Nat.dvd_sub (dvd_mul_right m n) dvd_rfl)).symm)
        (lt_of_lt_of_le hx le_tsub_add)

namespace Nat

open Submodule.IsPrincipal

/-- The gcd of a set of natural numbers is defined to be the nonnegative generator
of the ideal of `ℤ` generated by them. -/
noncomputable def setGcd (s : Set ℕ) : ℕ :=
  (generator <| Ideal.span <| ((↑) : ℕ → ℤ) '' s).natAbs

variable {s t : Set ℕ} {n : ℕ}

lemma setGcd_dvd_of_mem (h : n ∈ s) : setGcd s ∣ n := by
  rw [setGcd, ← Int.dvd_natCast, ← mem_iff_generator_dvd]
  exact Ideal.subset_span ⟨n, h, rfl⟩

lemma setGcd_dvd_of_mem_closure (h : n ∈ AddSubmonoid.closure s) : setGcd s ∣ n :=
  AddSubmonoid.closure_induction (fun _ ↦ setGcd_dvd_of_mem) (dvd_zero _) (fun _ _ _ _ ↦ dvd_add) h

/-- The characterizing property of `Nat.setGcd`. -/
lemma dvd_setGcd_iff : n ∣ setGcd s ↔ ∀ m ∈ s, n ∣ m := by
  simp_rw [setGcd, ← Int.natCast_dvd, dvd_generator_span_iff,
    Set.forall_mem_image, Int.natCast_dvd_natCast]

lemma setGcd_mono (h : s ⊆ t) : setGcd t ∣ setGcd s :=
  dvd_setGcd_iff.mpr fun _m hm ↦ setGcd_dvd_of_mem (h hm)

lemma dvdNotUnit_setGcd_insert (h : ¬ setGcd s ∣ n) :
    DvdNotUnit (setGcd (insert n s)) (setGcd s) :=
  dvdNotUnit_of_dvd_of_not_dvd (setGcd_mono <| Set.subset_insert ..)
    fun dvd ↦ h <| dvd_setGcd_iff.mp dvd _ (Set.mem_insert ..)

lemma setGcd_insert_of_dvd (h : setGcd s ∣ n) : setGcd (insert n s) = setGcd s :=
  (setGcd_mono <| Set.subset_insert ..).antisymm <| dvd_setGcd_iff.mpr
    fun m ↦ by rintro (rfl | hm); exacts [h, setGcd_dvd_of_mem hm]

lemma setGcd_eq_zero_iff : setGcd s = 0 ↔ s ⊆ {0} := by
  simp_rw [setGcd, Int.natAbs_eq_zero, ← eq_bot_iff_generator_eq_zero, Ideal.span_eq_bot,
    Set.forall_mem_image, Int.natCast_eq_zero, Set.subset_def, Set.mem_singleton_iff]

lemma exists_ne_zero_of_setGcd_ne_zero (hs : setGcd s ≠ 0) : ∃ n ∈ s, n ≠ 0 := by
  contrapose! hs
  exact setGcd_eq_zero_iff.mpr hs

variable (s)

lemma span_singleton_setGcd : Ideal.span {(setGcd s : ℤ)} = Ideal.span (((↑) : ℕ → ℤ) '' s) := by
  rw [setGcd, ← Ideal.span_singleton_eq_span_singleton.mpr (Int.associated_natAbs _),
    Ideal.span, span_singleton_generator]

lemma subset_span_setGcd : s ⊆ Ideal.span {setGcd s} :=
  fun _x hx ↦ Ideal.mem_span_singleton.mpr (setGcd_dvd_of_mem hx)

open Ideal in
theorem exists_mem_span_nat_finset_of_ge :
    ∃ (t : Finset ℕ) (n : ℕ), ↑t ⊆ s ∧ ∀ m ≥ n, setGcd s ∣ m → m ∈ Ideal.span t := by
  by_cases h0 : setGcd s = 0
  · refine ⟨∅, 0, by simp, fun _ _ dvd ↦ by cases zero_dvd_iff.mp (h0 ▸ dvd); exact zero_mem _⟩
  -- Write the gcd of `s` as a ℤ-linear combination of a finite subset `t`.
  have ⟨t, hts, a, eq⟩ := (Submodule.mem_span_image_iff_exists_fun _).mp
    (span_singleton_setGcd s ▸ mem_span_singleton_self _)
  -- Let `x` be an arbitrary nonzero element in `s`.
  have ⟨x, hxs, hx⟩ := exists_ne_zero_of_setGcd_ne_zero h0
  let n := (x / setGcd s) * ∑ i, (-a i).toNat * i
  refine ⟨insert x t, n, by simpa [Set.insert_subset_iff] using ⟨hxs, hts⟩, fun m ge dvd ↦ ?_⟩
  -- For `m ≥ n`, write `m = q * x + (r + n)` with 0 ≤ r < x.
  obtain ⟨c, rfl⟩ := exists_add_of_le ge
  rw [← c.div_add_mod' x]
  set q := c / x
  set r := c % x
  rw [add_comm, add_assoc]
  refine add_mem (mul_mem_left _ q (subset_span (Finset.mem_insert_self ..)))
    (Submodule.span_mono (s := t) (Finset.subset_insert ..) ?_)
  -- It suffices to show `r + n` lies in the ℕ-span of `t`.
  obtain ⟨rx, hrx⟩ : setGcd s ∣ r := (dvd_mod_iff (setGcd_dvd_of_mem hxs)).mpr <|
    (Nat.dvd_add_right <| dvd_mul_of_dvd_right (Finset.dvd_sum fun i _ ↦
      dvd_mul_of_dvd_right (setGcd_dvd_of_mem (hts i.2)) _) _).mp dvd
  convert (sum_mem fun i _ ↦ mul_mem_left _ _ (subset_span i.2) :
    -- an explicit ℕ-linear combination of elements of `t` that is equal to `r + n`
    ∑ i : t, (if 0 ≤ a i then rx else x / setGcd s - rx) * (a i).natAbs * i ∈ span t)
  simp_rw [← Int.natCast_inj, hrx, n, Finset.mul_sum, mul_comm _ rx, cast_add, cast_sum, cast_mul,
    ← eq, Finset.mul_sum, smul_eq_mul, ← mul_assoc, ← Finset.sum_add_distrib, ← add_mul]
  congr! 2 with i
  split_ifs with hai
  · rw [Int.toNat_eq_zero.mpr (by cutsat), cast_zero, mul_zero, add_zero,
      Int.natCast_natAbs, abs_eq_self.mpr hai]
  · rw [cast_sub, Int.natCast_natAbs, abs_eq_neg_self.mpr (by cutsat), sub_mul,
      ← Int.eq_natCast_toNat.mpr (by cutsat), mul_neg (rx : ℤ), sub_neg_eq_add, add_comm]
    rw [← Nat.mul_le_mul_left_iff (pos_of_ne_zero h0), ← hrx,
      Nat.mul_div_cancel' (setGcd_dvd_of_mem hxs)]
    exact (c.mod_lt (pos_of_ne_zero hx)).le

theorem exists_mem_closure_of_ge : ∃ n, ∀ m ≥ n, setGcd s ∣ m → m ∈ AddSubmonoid.closure s :=
  have ⟨_t, n, hts, hn⟩ := exists_mem_span_nat_finset_of_ge s
  ⟨n, fun m ge dvd ↦ (Submodule.span_nat_eq_addSubmonoidClosure s).le
    (Submodule.span_mono hts (hn m ge dvd))⟩

theorem finite_setOf_setGcd_dvd_and_mem_span :
    {n | setGcd s ∣ n ∧ n ∉ Ideal.span s}.Finite :=
  have ⟨n, hn⟩ := exists_mem_closure_of_ge s
  (Finset.range n).finite_toSet.subset fun m h ↦ Finset.mem_range.mpr <|
    lt_of_not_ge fun ge ↦ h.2 <| (Submodule.span_nat_eq_addSubmonoidClosure s).ge (hn m ge h.1)

/-- `ℕ` is a Noetherian `ℕ`-module, i.e., `ℕ` is a Noetherian semiring. -/
instance : IsNoetherian ℕ ℕ where
  noetherian s := by
    have ⟨t, n, hts, hn⟩ := exists_mem_span_nat_finset_of_ge s
    classical
    refine ⟨t ∪ {m ∈ Finset.range n | m ∈ s}, (Submodule.span_le.mpr ?_).antisymm fun m hm ↦ ?_⟩
    · simpa using ⟨hts, fun _ ↦ And.right⟩
    obtain le | gt := le_or_gt n m
    · exact Submodule.span_mono (by simp) (hn m le (setGcd_dvd_of_mem hm))
    · exact Submodule.subset_span (by simpa using .inr ⟨gt, hm⟩)

theorem addSubmonoid_fg (s : AddSubmonoid ℕ) : s.FG := by
  rw [← s.toNatSubmodule_toAddSubmonoid, ← Submodule.fg_iff_addSubmonoid_fg]
  apply IsNoetherian.noetherian

end Nat

/-- A set of natural numbers has a Frobenius number iff their gcd is 1; if 1 is in the set,
the Frobenius number is -1, so the Frobenius number doesn't exist as a natural number.
[Wikipedia](https://en.wikipedia.org/wiki/Coin_problem#Statement) seems to attribute this to
Issai Schur, but [Schur's theorem](https://en.wikipedia.org/wiki/Schur%27s_theorem#Combinatorics)
is a more precise statement about asymptotics of the number of ℕ-linear combinations, and the
existence of the Frobenius number for a set with gcd 1 is probably well known before that. -/
theorem exists_frobeniusNumber_iff {s : Set ℕ} :
    (∃ n, FrobeniusNumber n s) ↔ setGcd s = 1 ∧ 1 ∉ s where
  mp := fun ⟨n, hn⟩ ↦ by
    rw [frobeniusNumber_iff] at hn
    exact ⟨dvd_one.mp <| Nat.dvd_add_iff_right (setGcd_dvd_of_mem_closure (hn.2 (n + 1)
      (by omega))) (n := 1) |>.mpr (setGcd_dvd_of_mem_closure (hn.2 (n + 2) (by omega))),
      fun h ↦ hn.1 <| AddSubmonoid.closure_mono (Set.singleton_subset_iff.mpr h)
        (addSubmonoidClosure_one.ge ⟨⟩)⟩
  mpr h := by
    have ⟨n, hn⟩ := exists_mem_closure_of_ge s
    let P n := n ∉ AddSubmonoid.closure s
    have : P 1 := h.2 ∘ one_mem_closure_iff.mp
    classical
    refine ⟨findGreatest P n, frobeniusNumber_iff.mpr ⟨findGreatest_spec (P := P) (m := 1)
      (le_of_not_gt fun lt ↦ this (hn _ lt.le h.1.dvd)) this, fun k gt ↦ ?_⟩⟩
    obtain le | le := le_total k n
    · exact of_not_not (findGreatest_is_greatest gt le)
    · exact hn k le (h.1.dvd.trans <| one_dvd k)
